(*
CS520 Project
William Blair

The main interface for the generator.
*)

#define ATS_STALOADFLAG 0 // no need for staloading at run-time

%{#
#include "generator.cats"
%}

staload "schedule.sats"

staload "libats/SATS/parworkshop.sats"

(* The input type for a file. *)
absviewtype input (l:addr,n:int)

(* A runnable generator. *)
abst@ype generator

(* Any identifying data. *)
abst@ype label

(* Linked List Type. *)
abst@ype gen_list (a:t@ype)

fun{a:t@ype} gen_list_length(list:gen_list(a)) : int

(* This may be going overboard... *)
abst@ype gen_string

(* A Generator's Template. *)
abst@ype generator_template

(* The Generator's Synchronization Interface *)
abst@ype generator_lock (v:view) = $extype"pthread_mutex_t*"
abst@ype generator_cond (v:view) = $extype"pthread_cond_t*"

fun generator_lock_make{v:view} (pf: v | (* none *) ): generator_lock(v) = "generator_lock_make"

fun generator_lock_acquire{v:view} (lock: generator_lock v) : (v | void ) = "generator_lock_acquire"

fun generator_lock_release{v:view} (pf: v | lock: generator_lock v) : void = "generator_lock_release"

fun generator_cond_make{v:view} () : generator_cond(v) = "generator_cond_make"

fun generator_cond_wait {v:view}
  (pf: v | cond: generator_cond(v), lock: generator_lock (v) ) : (v | void) = "generator_cond_wait"

fun generator_cond_signal{v:view}
  (cond: generator_cond(v)) : void = "generator_cond_signal"
  
fun generator_cond_broadcast{v:view}
  (cond: generator_cond(v)) : void = "generator_cond_broadcast"

(* For Accessing Global Variables. *)
absprop generator_guard (v:view)

prfun generator_guard_make{v:view} (pf: v) : generator_guard(v)

prfun generator_guard_acquire{v:view} (guard: generator_guard(v)) : (v)

prfun generator_guard_release{v:view} (pf: v | guard: generator_guard(v) ) : void

(* Generator's Main Interface. *)

fun generator_setup() : void

fun load_file(filename : gen_string) : [l:addr][n:int] input(l,n)

fun input_parse_generators{l:addr}{n:int}(input: input(l,n)) : gen_list(generator)

fun generator_resource {l:addr} (
  ws: !WORKSHOPptr(generator,l),
  gen: &generator >> generator?
  ): int

fun generator_dispatch {l:addr | l > null} (
  ws: !WORKSHOPptr(generator,l),
  gens: gen_list(generator)
  ) : void

(* N-Party Rendezvous *)
fun generator_rendezvous () : void

fun generator_init (gen : !generator ) : void

fun generator_birth (
  gen : !generator, 
  shedule: !schedule(event)
  ) : void

fun generator_template_save(
  type:label, 
  gen: generator_template
  ) : void
  
fun generator_template_get(type:label) : generator_template

fun generator_template_parse(template:generator_template) : [l:addr] [n:int] input(l,n) -<cloref1> generator

fun generator_template_parse_label(type:label) : [l:addr][n:int]input(l,n) -<cloref1> generator

(* Why not just use pattern matching instead of this??  *)
fun generator_parse_cpu{l:addr}{n:int}(gen: input(l,n)) : generator

fun generator_parse_disk{l:addr}{n:int}(gen: input(l,n)) : generator

fun generator_parse_mem{l:addr}{n:int}(gen: input(l,n)) : generator

fun generator_parse_l1{l:addr}{n:int}(gen: input(l,n)) : generator

fun generator_parse_l2{l:addr}{n:int}(gen: input(l,n)) : generator

fun generator_parse_l3{l:addr}{n:int}(gen: input(l,n)) : generator
